$\forall$$A$:Type, $P$:($A$$\rightarrow\mathbb{N}\rightarrow\mathbb{B}$), $d$:($\forall$$x$:$A$. Dec($\exists$$n$:$\mathbb{N}$. ($\uparrow$($P$($x$,$n$))))), $x$:$A$.
\\[0ex]($\uparrow$can{-}apply(mu'($P$);$x$))
\\[0ex]$\Rightarrow$ \{($\uparrow$($P$($x$,do{-}apply(mu'($P$);$x$)))) \& ($\forall$$i$:\{0..do{-}apply(mu'($P$);$x$)$^{-}$\}. $\neg$($\uparrow$($P$($x$,$i$))))\}